PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 02:30:49 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 rabin.15.prism rabin.15.props --property live
Parsing model file "rabin.15.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15
Variables: c b r p1 b1 r1 draw1 p2 b2 r2 draw2 p3 b3 r3 draw3 p4 b4 r4 draw4 p5 b5 r5 draw5 p6 b6 r6 draw6 p7 b7 r7 draw7 p8 b8 r8 draw8 p9 b9 r9 draw9 p10 b10 r10 draw10 p11 b11 r11 draw11 p12 b12 r12 draw12 p13 b13 r13 draw13 p14 b14 r14 draw14 p15 b15 r15 draw15
Parsing properties file "rabin.15.props"...
1 property:
(1) "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 57 iterations in 201.95 seconds (average 3.542930, setup 0.00)
Time for model construction: 211.627 seconds.
Type: MDP
States: 1.517245861649857E21 (1 initial)
Transitions: 1.2795017806810437E22
Choices: 3.02320851799464E21
Transition matrix: 2007172 nodes (9 terminal), 1.2795017806810437E22 minterms, vars: 141r/141c/15nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 5 iterations in 2.07 seconds (average 0.413200, setup 0.00)
Prob1E: 6 iterations in 0.99 seconds (average 0.165667, setup 0.00)
yes = 1.517245861649857E21, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 3.647 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 215.674 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.